package prolog.terms

class Unfolder(prog: Prog, goal: List[Term], atClause: Iterator[List[Term]]) {
  type CLAUSE = List[Term]
  type GOAL = List[Term]

  val trail = prog.trail
  val oldtop = trail.size

  def notLastClause = atClause.hasNext

  private final def unfold(gs: GOAL, cs: CLAUSE, trail: Trail): GOAL = {
    trail.unwind(oldtop)

    gs match {
      case Nil => Nil
      case g :: xs => {
        if (cs.head.matches(g, trail)) {
          val ds = Term.copyList(cs)
          ds.head.unify(g, trail)
          ds.tail ++ xs
        } else
          null
      }
    }

    // Nil: no more work
    // null: we have failed
  }

  def nextGoal(): GOAL = {
    var newgoal: GOAL = null
    while (newgoal.eq(null) && atClause.hasNext) {
      val clause: CLAUSE = atClause.next
      newgoal = unfold(goal, clause, trail)
    }
    newgoal
  }

  override def toString = "Step:" + goal
}

